FDL - Step of Proof: do-apply-p-co-filter

Step of Proof: do-apply-p-co-filter

11,40

Inference at *
Iof proof for Lemma do-apply-p-co-filter:

T:Type, P:(T

), f:(

x:T. Dec(P(x))), x:T.

(

can-apply(p-co-filter(f);x))

(do-apply(p-co-filter(f);x) = x)

by (((if (((first_nat 4:n)) = 0) then (Repeat (((D (0)

)
CollapseTHENA (Auto

))

Co)) else (RepeatFor (first_nat 4:n) (((D (0)

)
CollapseTHENA (Auto

))

)))

)
CollapseTHEN (
CoRepUR ``can-apply do-apply p-co-filter`` ( 0)

))

Co1:

Co1: 1. T : Type
Co1: 2. P : T

Co1: 3. f :

x:T. Dec(P(x))
Co1: 4. x : T
Co1:

(

isl(case f(x) of inl(p) => inr p | inr(p) => inl x ))
Co1:

(outl(case f(x) of inl(p) => inr p | inr(p) => inl x ) = x)
Co.

Definitions , Type, Dec(P), x(s), f(a), x:A. B(x), P Q, s = t, x:AB(x), can-apply(f;x), p-co-filter(f), do-apply(f;x), b